ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(x, y), 0)
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(x, y), 0)
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
AP(ap(ap(g, x), y), ap(s, z)) → AP(x, y)
Used ordering: Polynomial interpretation [25,35]:
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
The value of delta used in the strict ordering is 15/16.
POL(ap(x1, x2)) = 3/2 + (1/4)x_1 + (4)x_2
POL(f) = 0
POL(AP(x1, x2)) = (1/2)x_1
POL(g) = 0
POL(s) = 0
POL(0) = 1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
AP(ap(ap(g, x), y), ap(s, z)) → AP(ap(ap(g, x), y), ap(ap(x, y), 0))
ap(f, x) → x
ap(ap(ap(g, x), y), ap(s, z)) → ap(ap(ap(g, x), y), ap(ap(x, y), 0))